In set theory, the support of a set turns the set into a subsingleton. In dependent type theory, propositional truncation or the bracket type is an operation which takes a type and turns it into a h-propositions, which are the type theoretic equivalent of subsingletons. By the relation between type theory and category theory and the relation between set theory and topos theory, it should be possible to do the same process and turn an object of a category into a subterminal object. These are the support objects, bracket objects, or propositional truncation objects in category theory.
The support object of an object in a regular category is the image of the unique morphism into the terminal object .
As a result, that all support objects exist is equivalent to the condition that every morphism into the terminal object has an image factorization.
The support object of an object in a unitary tabular allegory is the tabulation? of the unique map from into the allegorical unit .
In any well-pointed pretopos , the support is the coequalizer of the product projection morphisms and
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Last revised on July 28, 2024 at 18:04:09. See the history of this page for a list of all contributions to it.